\begin{tabbing} $\forall$\=$A$:Type, $I$:MaInterface($A$), $i$:\{$i$:Id$\mid$ ($i$ $\in$ fpf{-}domain($I$))\} ,\+ \\[0ex]$k$:\{$k$:Knd$\mid$ ($k$ $\in$ fpf{-}domain($I$($i$).2))\} . \-\\[0ex]($I$($i$).2($k$).2) $\in$ State($I$($i$).1)$\rightarrow$($I$($i$).2($k$).1)$\rightarrow$($A$ + Top) \end{tabbing}